
@Book{		  Avig14,
  author	= "Avigad, Jeremy and {de Moura}, Leonardo and Kong, Soonho",
  title		= {{Theorem Proving in Lean}},
  year		= "2014",
  link		= "\url{https://leanprover.github.io/tutorial/tutorial.pdf}",
  publisher	= "Carnegie Mellon University"
}

@Book{		  Avig17,
  author	= "Avigad, Jeremy and Lewis, Robert Y. and {van Doorn},
		  Floris",
  title		= {{Logic and Proof}},
  year		= "2017",
  link		= "\url{https://avigad.github.io/logic_and_proof}",
  publisher	= "Carnegie Mellon University"
}

@InProceedings{	  AvigadCarneiroHudon19,
  author	= {Jeremy Avigad and Mario M. Carneiro and Simon Hudon},
  title		= {Data Types as Quotients of Polynomial Functors},
  booktitle	= {10th International Conference on Interactive Theorem
		  Proving, {ITP} 2019, September 9-12, 2019, Portland, OR,
		  {USA}},
  pages		= {6:1--6:19},
  year		= {2019},
  url		= {https://doi.org/10.4230/LIPIcs.ITP.2019.6},
  doi		= {10.4230/LIPIcs.ITP.2019.6},
  timestamp	= {Fri, 27 Sep 2019 15:57:06 +0200},
  biburl	= {https://dblp.org/rec/conf/itp/AvigadCH19.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@Article{	  Baanen20,
  author	= {Anne Baanen},
  title		= {A Lean tactic for normalising ring expressions with
		  exponents},
  url		= {https://lean-forward.github.io/ring_exp/paper.pdf},
  note		= {IJCAR 2020},
  year		= {2020}
}

@InProceedings{	  Buch18,
  author	= {Ulrik Buchholtz and Floris {van Doorn} and Egbert Rijke},
  title		= {Higher Groups in Homotopy Type Theory},
  booktitle	= {Proceedings of the 33rd Annual {ACM/IEEE} Symposium on
		  Logic in Computer Science, {LICS} 2018, Oxford, UK, July
		  09-12, 2018},
  pages		= {205--214},
  year		= {2018},
  crossref	= {DBLP:conf/lics/2018},
  url		= {https://doi.org/10.1145/3209108.3209150},
  doi		= {10.1145/3209108.3209150}
}

@InProceedings{	  BuzzardCommelinMassot20,
  author	= {Kevin Buzzard and Johan Commelin and Patrick Massot},
  title		= {Formalising perfectoid spaces},
  booktitle	= {Proceedings of the 9th {ACM} {SIGPLAN} International
		  Conference on Certified Programs and Proofs, {CPP} 2020,
		  New Orleans, LA, USA, January 20-21, 2020},
  pages		= {299--312},
  year		= {2020},
  url		= {https://doi.org/10.1145/3372885.3373830},
  doi		= {10.1145/3372885.3373830},
  timestamp	= {Thu, 23 Jan 2020 16:12:31 +0100},
  biburl	= {https://dblp.org/rec/conf/cpp/BuzzardCM20.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  Carneiro19,
  author	= {Mario M. Carneiro},
  title		= {Formalizing Computability Theory via Partial Recursive
		  Functions},
  booktitle	= {10th International Conference on Interactive Theorem
		  Proving, {ITP} 2019, September 9-12, 2019, Portland, OR,
		  {USA}},
  pages		= {12:1--12:17},
  year		= {2019},
  url		= {https://doi.org/10.4230/LIPIcs.ITP.2019.12},
  doi		= {10.4230/LIPIcs.ITP.2019.12},
  timestamp	= {Fri, 27 Sep 2019 15:57:06 +0200},
  biburl	= {https://dblp.org/rec/conf/itp/Carneiro19.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@Misc{		  CarneiroMaster,
  author	= {Mario Carneiro},
  title		= {The Type Theory of Lean},
  eprint	= {https://github.com/digama0/lean-type-theory/releases},
  note		= {Master thesis},
  year		= {2019},
  abstract	= {Meta-theoretic properties of Lean 3, including
		  soundness.}
}

@InProceedings{	  DahmenHolzlLewis19,
  author	= {Sander R. Dahmen and Johannes H{\"{o}}lzl and Robert Y.
		  Lewis},
  title		= {Formalizing the Solution to the Cap Set Problem},
  booktitle	= {10th International Conference on Interactive Theorem
		  Proving, {ITP} 2019, September 9-12, 2019, Portland, OR,
		  {USA}},
  pages		= {15:1--15:19},
  year		= {2019},
  url		= {https://doi.org/10.4230/LIPIcs.ITP.2019.15},
  doi		= {10.4230/LIPIcs.ITP.2019.15},
  timestamp	= {Mon, 23 Sep 2019 17:27:15 +0200},
  biburl	= {https://dblp.org/rec/conf/itp/DahmenHL19.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@Misc{		  DeMoura15,
  author	= "{de Moura}, Leonardo and Avigad, Jeremy and Kong, Soonho
		  and Roux, Cody",
  title		= {{Elaboration in Dependent Type Theory}},
  link		= "\url{https://arxiv.org/pdf/1505.04324.pdf}",
  year		= "2015",
  abstract	= {Elaboration in Lean 2}
}

@InProceedings{	  DeMouraKongAvigadVanDoornvonRaumer,
  author	= {Leonardo Mendonça {de Moura} and Soonho Kong and Jeremy
		  Avigad and Floris {van Doorn} and Jakob {von Raumer}},
  title		= {The Lean Theorem Prover (System Description)},
  booktitle	= {Automated Deduction - CADE-25 - 25th International
		  Conference on Automated Deduction, Berlin, Germany, August
		  1-7, 2015, Proceedings},
  pages		= {378--388},
  year		= {2015},
  crossref	= {DBLP:conf/cade/2015},
  url		= "\url{https://doi.org/10.1007/978-3-319-21401-6_26}",
  doi		= {10.1007/978-3-319-21401-6\_26},
  timestamp	= {Tue, 14 May 2019 10:00:39 +0200},
  biburl	= {https://dblp.org/rec/conf/cade/MouraKADR15.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org},
  abstract	= {System description of Lean 2}
}

@InProceedings{	  Door16,
  author	= {Floris {van Doorn}},
  title		= {Constructing the propositional truncation using
		  non-recursive HITs},
  booktitle	= {Proceedings of the 5th {ACM} {SIGPLAN} Conference on
		  Certified Programs and Proofs, Saint Petersburg, FL, USA,
		  January 20-22, 2016},
  pages		= {122--129},
  year		= {2016},
  crossref	= {DBLP:conf/cpp/2016},
  url		= {https://doi.org/10.1145/2854065.2854076},
  doi		= {10.1145/2854065.2854076},
  timestamp	= {Tue, 06 Nov 2018 16:59:23 +0100},
  biburl	= {https://dblp.org/rec/bib/conf/cpp/Doorn16},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  Door17,
  author	= {Floris {van Doorn} and Jakob {von Raumer} and Ulrik
		  Buchholtz},
  title		= {Homotopy Type Theory in Lean},
  booktitle	= {Interactive Theorem Proving - 8th International
		  Conference, {ITP} 2017, Bras{\'{\i}}lia, Brazil, September
		  26-29, 2017, Proceedings},
  pages		= {479--495},
  year		= {2017},
  crossref	= {DBLP:conf/itp/2017},
  url		= "\url{https://doi.org/10.1007/978-3-319-66107-0_30}",
  doi		= {10.1007/978-3-319-66107-0\_30},
  timestamp	= {Tue, 14 May 2019 10:00:37 +0200},
  biburl	= {https://dblp.org/rec/bib/conf/itp/DoornRB17},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@Article{	  EURAM17,
  author	= {Gabriel Ebner and Sebastian Ullrich and Jared Roesch and
		  Jeremy Avigad and Leonardo {de Moura}},
  title		= {A metaprogramming framework for formal verification},
  journal	= {{PACMPL}},
  volume	= {1},
  number	= {{ICFP}},
  pages		= {34:1--34:29},
  year		= {2017},
  url		= {https://doi.org/10.1145/3110278},
  doi		= {10.1145/3110278},
  timestamp	= {Tue, 06 Nov 2018 12:51:05 +0100},
  biburl	= {https://dblp.org/rec/bib/journals/pacmpl/EbnerURAM17},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@Misc{		  FernandezMir19,
  author	= {Ramon Fernández Mir},
  title		= {Schemes in Lean},
  eprint	= {https://www.imperial.ac.uk/media/imperial-college/faculty-of-engineering/computing/public/1819-ug-projects/Fernandez-I-MirR-Schemes-in-Lean.pdf},
  note		= {Project report},
  year		= {2019}
}

@InProceedings{	  HanVanDoorn,
  author	= {Jesse Michael Han and Floris {van Doorn}},
  title		= {A formal proof of the independence of the continuum
		  hypothesis},
  booktitle	= {Proceedings of the 9th {ACM} {SIGPLAN} International
		  Conference on Certified Programs and Proofs, {CPP} 2020,
		  New Orleans, LA, USA, January 20-21, 2020},
  pages		= {353--366},
  year		= {2020},
  url		= {https://doi.org/10.1145/3372885.3373826},
  doi		= {10.1145/3372885.3373826},
  timestamp	= {Thu, 23 Jan 2020 16:12:31 +0100},
  biburl	= {https://dblp.org/rec/conf/cpp/HanD20.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  HanVanDoorn19,
  author	= {Jesse Michael Han and Floris {van Doorn}},
  title		= {A Formalization of Forcing and the Unprovability of the
		  Continuum Hypothesis},
  booktitle	= {10th International Conference on Interactive Theorem
		  Proving, {ITP} 2019, September 9-12, 2019, Portland, OR,
		  {USA}},
  pages		= {19:1--19:19},
  year		= {2019},
  crossref	= {DBLP:conf/itp/2019},
  url		= {https://doi.org/10.4230/LIPIcs.ITP.2019.19},
  doi		= {10.4230/LIPIcs.ITP.2019.19},
  timestamp	= {Sat, 07 Sep 2019 02:31:13 +0200},
  biburl	= {https://dblp.org/rec/conf/itp/HanD19.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@Misc{		  Huisinga19,
  author	= {Marc Huisinga},
  title		= {Formally Verified Insertion of Reference Counting
		  Instructions},
  eprint	= {https://pp.ipd.kit.edu/uploads/publikationen/huisinga19bachelorarbeit.pdf},
  note		= {Bachelor thesis},
  year		= {2019}
}

@InProceedings{	  LeeHurLopes19,
  author	= {Juneyoung Lee and Chung{-}Kil Hur and Nuno P. Lopes},
  title		= {AliveInLean: {A} Verified {LLVM} Peephole Optimization
		  Verifier},
  booktitle	= {Computer Aided Verification - 31st International
		  Conference, {CAV} 2019, New York City, NY, USA, July 15-18,
		  2019, Proceedings, Part {II}},
  pages		= {445--455},
  year		= {2019},
  url		= "\url{https://doi.org/10.1007/978-3-030-25543-5_25}",
  doi		= {10.1007/978-3-030-25543-5\_25},
  timestamp	= {Fri, 27 Mar 2020 08:45:57 +0100},
  biburl	= {https://dblp.org/rec/conf/cav/LeeHL19.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  Lewis17,
  author	= {Robert Y. Lewis},
  title		= {An Extensible Ad Hoc Interface between Lean and
		  Mathematica},
  booktitle	= {Proceedings of the Fifth Workshop on Proof eXchange for
		  Theorem Proving, PxTP 2017, Bras{\'{\i}}lia, Brazil, 23-24
		  September 2017},
  pages		= {23--37},
  year		= {2017},
  url		= {https://doi.org/10.4204/EPTCS.262.4},
  doi		= {10.4204/EPTCS.262.4},
  timestamp	= {Wed, 12 Sep 2018 01:05:13 +0200},
  biburl	= {https://dblp.org/rec/journals/corr/abs-1712-09288.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  Lewis19,
  author	= {Robert Y. Lewis},
  title		= {A formal proof of {H}ensel's lemma over the p-adic
		  integers},
  booktitle	= {Proceedings of the 8th {ACM} {SIGPLAN} International
		  Conference on Certified Programs and Proofs, {CPP} 2019,
		  Cascais, Portugal, January 14-15, 2019},
  pages		= {15--26},
  year		= {2019},
  crossref	= {DBLP:conf/cpp/2019},
  url		= {https://doi.org/10.1145/3293880.3294089},
  doi		= {10.1145/3293880.3294089},
  timestamp	= {Fri, 04 Jan 2019 10:46:45 +0100},
  biburl	= {https://dblp.org/rec/bib/conf/cpp/Lewis19},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  LewisMadelaine20,
  author	= {Robert Y. Lewis and Paul{-}Nicolas Madelaine},
  title		= {Simplifying Casts and Coercions},
  booktitle	= {Practical Aspects of Automated Reasoning, {PAAR} 2020},
  year		= {2020},
  url		= {https://arxiv.org/abs/2001.10594},
  archiveprefix	= {arXiv},
  eprint	= {2001.10594},
  timestamp	= {Thu, 30 Jan 2020 18:46:36 +0100},
  biburl	= {https://dblp.org/rec/journals/corr/abs-2001-10594.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@Article{	  Madelaine19,
  author	= {Paul{-}Nicolas Madelaine},
  title		= {Arithmetic and Casting in Lean},
  url		= {https://lean-forward.github.io/norm_cast/norm_cast.pdf},
  year		= {2019}
}

@InProceedings{	  Mathlib,
  title		= {The {L}ean mathematical library},
  booktitle	= {Proceedings of the 9th {ACM} {SIGPLAN} International
		  Conference on Certified Programs and Proofs, {CPP} 2020,
		  New Orleans, LA, USA, January 20-21, 2020},
  author	= {{The mathlib community}},
  pages		= {367--381},
  year		= {2020},
  url		= {https://doi.org/10.1145/3372885.3373824},
  doi		= {10.1145/3372885.3373824},
  timestamp	= {Thu, 23 Jan 2020 16:12:31 +0100},
  biburl	= {https://dblp.org/rec/conf/cpp/X20.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@Article{	  SelsamDeMoura16,
  author	= {Daniel Selsam and Leonardo {de Moura}},
  title		= {Congruence Closure in Intensional Type Theory},
  booktitle	= {Automated Reasoning - 8th International Joint Conference,
		  {IJCAR} 2016, Coimbra, Portugal, June 27 - July 2, 2016,
		  Proceedings},
  pages		= {99--115},
  year		= {2016},
  crossref	= {DBLP:conf/cade/2016},
  url		= "\url{https://doi.org/10.1007/978-3-319-40229-1_8}",
  doi		= {10.1007/978-3-319-40229-1\_8},
  timestamp	= {Wed, 06 Nov 2019 16:45:49 +0100},
  biburl	= {https://dblp.org/rec/conf/cade/SelsamM16.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@Misc{		  SelsamHudonDeMoura20,
  author	= {Daniel Selsam and Simon Hudon and Leonardo {de Moura}},
  title		= {Sealing Pointer-Based Optimizations Behind Pure
		  Functions},
  year		= {2020},
  eprint	= {arXiv:2003.01685}
}

@InProceedings{	  SelsamLD17,
  author	= {Daniel Selsam and Percy Liang and David L. Dill},
  title		= {Developing Bug-Free Machine Learning Systems With Formal
		  Mathematics},
  booktitle	= {Proceedings of the 34th International Conference on
		  Machine Learning, {ICML} 2017, Sydney, NSW, Australia, 6-11
		  August 2017},
  pages		= {3047--3056},
  year		= {2017},
  crossref	= {DBLP:conf/icml/2017},
  url		= {http://proceedings.mlr.press/v70/selsam17a.html},
  timestamp	= {Wed, 29 May 2019 08:41:45 +0200},
  biburl	= {https://dblp.org/rec/bib/conf/icml/SelsamLD17},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@Misc{		  SelsamUllrichDeMoura20,
  author	= {Daniel Selsam and Sebastian Ullrich and Leonardo {de
		  Moura}},
  title		= {Tabled Typeclass Resolution},
  year		= {2020},
  eprint	= {arXiv:2001.04301}
}

@Misc{		  StricklandBellumat19,
  author	= {Neil Strickland and Nicola Bellumat},
  title		= {Iterated chromatic localisation},
  year		= {2019},
  eprint	= {arXiv:1907.07801}
}

@Misc{		  Ullrich16,
  author	= {Sebastian Ullrich},
  title		= {Simple Verification of {R}ust Programs via Functional
		  Purification},
  eprint	= {https://github.com/Kha/masters-thesis/blob/master/main.pdf},
  note		= {Masters thesis},
  year		= {2016}
}

@Article{	  UllrichDeMoura19,
  author	= {Sebastian Ullrich and Leonardo {de Moura}},
  title		= {Counting Immutable Beans: Reference Counting Optimized for
		  Purely Functional Programming},
  year		= {2019},
  url		= {http://arxiv.org/abs/1908.05647},
  archiveprefix	= {arXiv},
  eprint	= {1908.05647}
}

@Misc{		  UllrichDeMoura20,
  author	= {Sebastian Ullrich and Leonardo {de Moura}},
  title		= {Beyond Notations: Hygienic Macro Expansion for Theorem
		  Proving Languages},
  year		= {2020},
  eprint	= {arXiv:2001.10490},
  abstract	= {The new type class resolution procedure in Lean 4.}
}

@InProceedings{	  VanDoornEbnerLewis20,
  author	= {Floris {van Doorn} and Gabriel Ebner and Robert Y. Lewis},
  title		= {Maintaining a Library of Formal Mathematics},
  booktitle	= {Intelligent Computer Mathematics, CICM 2020},
  volume	= {abs/2004.03673},
  year		= {2020},
  url		= {https://arxiv.org/abs/2004.03673},
  archiveprefix	= {arXiv},
  eprint	= {2004.03673},
  timestamp	= {Tue, 14 Apr 2020 16:40:34 +0200},
  biburl	= {https://dblp.org/rec/journals/corr/abs-2004-03673.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@Misc{		  VonRaumer15,
  author	= {Jakob {von Raumer}},
  title		= {Formalization of Non-Abelian Topology for Homotopy Type
		  Theory},
  eprint	= {http://www.contrib.andrew.cmu.edu/~avigad/Students/von_raumer_thesis.pdf},
  note		= {Masters thesis},
  year		= {2015}
}

@InProceedings{	  VonRaumer16,
  author	= {Jakob {von Raumer}},
  title		= {Formalizing Double Groupoids and Cross Modules in the Lean
		  Theorem Prover},
  booktitle	= {Mathematical Software - {ICMS} 2016 - 5th International
		  Conference, Berlin, Germany, July 11-14, 2016,
		  Proceedings},
  pages		= {28--33},
  year		= {2016},
  crossref	= {DBLP:conf/icms/2016},
  url		= "\url{https://doi.org/10.1007/978-3-319-42432-3_4}",
  doi		= {10.1007/978-3-319-42432-3\_4},
  timestamp	= {Tue, 14 May 2019 10:00:40 +0200},
  biburl	= {https://dblp.org/rec/bib/conf/icms/Raumer16},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}

@InProceedings{	  WuGore19,
  author	= {Minchao Wu and Rajeev Gor{\'{e}}},
  title		= {Verified Decision Procedures for Modal Logics},
  booktitle	= {10th International Conference on Interactive Theorem
		  Proving, {ITP} 2019, September 9-12, 2019, Portland, OR,
		  {USA}},
  pages		= {31:1--31:19},
  year		= {2019},
  url		= {https://doi.org/10.4230/LIPIcs.ITP.2019.31},
  doi		= {10.4230/LIPIcs.ITP.2019.31},
  timestamp	= {Mon, 23 Sep 2019 17:27:15 +0200},
  biburl	= {https://dblp.org/rec/conf/itp/WuG19.bib},
  bibsource	= {dblp computer science bibliography, https://dblp.org}
}
